Inference at * 1 
Iof proof for Lemma squash functionality wrt implies:



1. P : 
2. Q : 
3. P  Q
4. P
  Q 

latex

 by ((((((D 4) 
CollapseTHEN (D 0))) 
CollapseTHEN (D 3))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, True, T, P  Q